$\forall$$T$:Type, ${\it eq}$:($T$$\rightarrow$$T$$\rightarrow\mathbb{B}$), $f$:($\mathbb{N}\rightarrow$$T$), $x$:$T$, $j$:$\mathbb{N}$. \#\{i$<$$j$$\mid$$f$ i ${\it eq}$ $x$\} $\in$ \{0..($j$+1)$^{-}$\}